佐々木勝一; "日本語定理証明支援系 かたぱ"
https://katapa.app
Calculus of Constructions
ベースの（
Coq
と同じ？）の
定理証明支援系
．
OcaML
で書こうとしたが断念して
TypeScript
で書いている．